Automated Mutual Explicit Induction Proof in Separation Logic

摘要

We present a sequent-based deductive system for automatically provingentailments in separation logic by using mathematical induction. Our technique,called mutual explicit induction proof, is an instance of Noetherian induction.Specifically, we propose a novel induction principle on a well-founded relationof separation logic model and follow the explicit induction methods toimplement this principle as inference rules, so that it can be easilyintegrated into a deductive system. We also support mutual induction, a naturalfeature of implicit induction, where the goal entailment and other entailmentsderived during the proof search can be used as hypotheses to prove each other.We have implemented a prototype prover and evaluated it on a benchmark ofhandcrafted entailments as well as benchmarks from a separation logiccompetition.